[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

I know this is still WIP, but could this not cause issues when taking the opposite of a strict bicategory? Then e.g. Catᵒᵖ has two category structures, one coming from the (strict) opposite bicategory, and one coming from the opposite underlying category. At some point last year I was also thinking about the opposite bicategory and I thought that one should have another type synonym to talk about this one, but maybe this is not an actual issue? I'm curious because I plan to clean up some old code on 2-Yoneda and in this case I need to talk about the opposite bicategory.

It seems to me that both instances are defeq:

-- TODO: `Strict C` implies `Strict Cᵒᵖ`:
example {C : Type*} [Bicategory C] [Strict C] [Strict Cᵒᵖ] :
    @StrictBicategory.category Cᵒᵖ Bicategory.Opposite.instOpposite _ =
      @Category.opposite C (StrictBicategory.category C) := 
  rfl

Okay great!

Then I will try to copy your approach for when I work on 2-Yoneda

Actually, have I understood correctly in that you are definining the "coop" dual (as in here). So you are dualizing both the 1-cells and the 2-cells?

Yes, this is dualizing both. TBH, it did not occur to me when writing this to only dualize the 1-cells, I just made this quickly to make the second forgetful functor from the bicategory of adjunctions type check. Probably we should have both versions separately? And then this one can be obtained by chaining them without losing any def-eqs?

Yes we should! I actually made the 1-cell dual a year ago locally, and I opened a PR here: #25901 once I understood that it wasn't duplicating this work here :) However I am trying to refactor it by making ^op work for CategoryStructs, but this is annoying since porting some of the basic API to that setting breaks some things in the library.

Instead of using families of morphisms, how about using Mathlib’s (Pre)Sieve? Since Grothendieck topologies in Mathlib are expressed in terms of sets of Sieves, we can make direct use of this.

This would be problematic because with the "family of maps" definition, we may happen to have two equal maps in the family, and this would not be an issue when defining an object in the descent data category, but it would be very ackward in the presieve approach. (This is already a little bit ackward for sheaves, and I have expanded the sheaf API to have more definitions/lemmas for families of morphisms for this reason!) We can make a definition for presieves as a particular case of our definition for families of maps. Eventually, there will be definitions saying that if two families of maps generate the same sieve, then the descent data categories are equivalent.

Thank you for explaining the advantages of using families of morphisms. I haven’t fully digested it yet, but do I understand correctly that what you mean is: it’s simpler to apply a definition for a family of morphisms to a presieve than to apply a definition for a presieve for a family of morphism?

we may happen to have two equal maps in the family

Strictly speaking, X i and X j are not definitionally equal when i and j are not, so f i and f j never become the same morphism, right? That is, a family of morphisms can be seen as an unfolded version of a presieve.

No, an indexed family contains strictly more data than a Presieve. Presieve.ofArrows of an indexed families is the "injectification" of the indexed family.

I view indexed families as the mathematically correct object to consider. Presieves are essentially an implementation detail. The only reason the basic object of the (pre)sieves library is not an indexed family (i.e. a PreZeroHypercover) is a universe issue (we don't want GrothendieckTopology etc. to carry an additional universe parameter).

Presieves are generally hard to manipulate, for example try binding a family of presieves on the components of a Presieve of the form Presieve.ofArrows using Presieve.bind! This leads to auxiliary definitions like Presieve.bindOfArrows (which is NOT equal to the obvious Presieve.ofArrows indexed by the sigma type).
In the language of indexed covers, this is very natural (see PreZeroHypercover.bind).
More generally, whenever you need to construct data for every morphism of a cover, it becomes very difficult when using presieves. The main reason being that you can't extract the index out of Presieve.ofArrows Y f g (the index is not even unique, by what I have explained above).
And in this sequence of PRs, we need to construct a lot of data!

Thank you for giving an example.

No, an indexed family contains strictly more data than a Presieve.

Yes, and also contains another universe as you mentioned.

I don’t have an opinion on whether presieves or indexed families are the “correct” notion (though sieves surely are). But I do think that matters of convenience are important, and your example may also convince me that indexed families are convenient for constructing sieves.

So basically, the strategy is to work with indexed families as much as possible, and only convert to a sieve via .ofArrows at the stage where one wants to eliminate the universe?

Yes. And note that most of the results and API developed here don't mention any GrothendieckTopology so no conversion between families and (pre)sieves is required.
Only in the last step for the definition of the condition IsStack we need to interact with GrothendieckTopology and hence sieves.

I personally prefer the more minimal approach of giving only an isomorphism from f i to q, without using f j, as the first definition. To me, this feels like a more basic definition. What do you think?

obj {Xᵢ : C} (fᵢ : Xᵢ ⟶ S) (_ : P fᵢ := by aesop_cat), F.obj (.mk (op Xᵢ))
iso ⦃Y : C⦄ (q : Y ⟶ S) ⦃Xᵢ : C⦄ (f : Y ⟶ Xᵢ) (fᵢ : Xᵢ ⟶ S)
  (_ : P fᵢ := by aesop_cat) (_ : P q := by aesop_cat)
  (_hf : f ≫ fᵢ = q := by aesop_cat) :
  (Fmap f.op.toLoc).obj (obj fᵢ) ≅ obj q

Here, P : Presieve S (or P : Sieve S so that P q is automatic). The original hom can then be recovered as the composition of iso q f₁ (f i₁) with the inverse of iso q f₂ (f i₂).

This may be mathematically sound only in the case P is a sieve. Again, working with families of morphisms as compared to (pre)sieves seem much more practical to me. (I feel that a lot of things that Christian and I have experienced successfully with our definitions would be much more inconvenient with your suggestion.)

Yes, this may be a "shortcut" that can be applied for sieve. When using a family of maps, it makes sense to me that "square diagram" is the minimal choice.

I feel that a lot of things that Christian and I have experienced successfully with our definitions would be much more inconvenient with your suggestion.

Could you provide some examples?

I gave examples above.